| Definitions | t  T, ES, AbsInterface(A), E(X), x:A  B(x), e c e',  x:A. B(x), l1 l2, P   Q, x:A  B(x),  b, left + right, P  Q, (e < e'), {x:A| B(x)} ,  x:A. B(x), Top, prior-f-fixedpoints(e), (x l), let x,y = A in B(x;y), t.1, a:A fp B(a), strong-subtype(A;B), Dec(P), (e <loc e'), e loc e' , e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e),  , a < b, {T}, n+m, False, Type,  ,  , Outcome, #$n, A B,  , Void,  A,  , S  T, n - m, |g|, e < e', SWellFounded(R(x;y)), e  X, EState(T), Id, EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r s, constant_function(f;A;B), pred!(e;e'),   x,y. t(x;y),  x:A.B(x), suptype(S; T), first(e), <a, b>, pred(e), x.A(x), x. t(x), P & Q, i  j , -n, f(a), E, s = t, [], A c B, l[i], ||as||, as @ bs, f(x)?z, P  Q, P Q, inl x , tt, inr x , ff, SQType(T), s ~ t, f g, IsPrimeIdeal(R;P), IsIntegDom(r), a b, IsMonHom{M1,M2}(f), IsGroup(T;op;id;inv), IsMonoid(T;op;id), monot(T;x,y.R(x;y);f), Cancel(T;S;op), FunThru2op(A;B;opa;opb;f), fun_thru_1op(A;B;opa;opb;f), Dist1op2opLR(A;1op;2op), IsAction(A;x;e;S;f), IsBilinear(A;B;C;+a;+b;+c;f), BiLinear(T;pl;tm), Inverse(T;op;id;inv), Comm(T;op), Assoc(T;op), Ident(T;op;id), CoPrime(a,b), Connex(T;x,y.R(x;y)), AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), IsEqFun(T;eq), Inj(A;B;f), InvFuns(A;B;f;g), a =!x:T. Q(x), SqStable(P), l_disjoint(T;l1;l2), q-rel(r;x), r < s, (xL.P(x)), xL. P(x), x f y, a < b, a <p b, a b, a ~ b, b | a,  T, True, if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), e = e', p q, p q, p q, b, deq-member(eq;x;L), a = b, a = b, qeq(r;s), q_less(a;b), q_le(r;s), eq_atom$n(x;y), [d], a < b, a < b, null(as), x =a y, (i = j), i z j, i <z j, p =b q, X(e), prior(X), [car / cdr], A List , sender(e), f**(e) |
| Lemmas | es-fix-equal, es-fix-causle, es-prior-fixedpoints-fix, es-fix wf2, member singleton, es-prior-interface-causl, iseg append, member append, es-interface-val wf, es-prior-interface wf, es-interface-val wf2, bnot wf, assert-es-eq-E-2, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, bool sq, bool cases, decidable assert, sq stable from decidable, bfalse wf, btrue wf, true wf, append wf, iseg weakening, es-prior-fixedpoints wf, select wf, length wf1, ge wf, nat properties, deq wf, EOrderAxioms wf, kind wf, Msg wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, first wf, unit wf, pred! wf, strongwellfounded wf, rationals wf, Id wf, EState wf, event system wf, es-interface wf, assert wf, es-is-interface wf, top wf, es-causle wf, es-causl-swellfnd, nat ind tp, guard wf, es-causl wf, le wf, false wf, nat wf, iseg wf, l member wf, decidable es-E-equal, es-E-interface-subtype rel, member wf, es-E wf, es-E-interface wf, subtype rel wf |
